Nuprl Lemma : comb_for_rng_sum_wf
13,42
postcript
pdf
(
r
,
p
,
q
,
E
,
z
.
(
r
)
p
i
<
q
.
E
(
i
))
r
:Rng
p
,
q
:
({
p
..
q
}
|
r
|)
(
True)
|
r
|
latex
Up
rings
1
Definitions of Statement
Rng
Definitions
t
T
,
,
x
:
A
.
B
(
x
)
,
T
,
Rng
Lemmas
rng
wf
,
rng
car
wf
,
int
seg
wf
,
true
wf
,
squash
wf
,
rng
sum
wf
origin
r,p,q,E,z. 
(r) p 
i < q. E(i)) 
r:Rng
p,q:
({p..q
}|r|)(
True)|r| r,p,q,E,z. (r) p i < q. E(i)) r:Rngp,q:({p..q}|r|)(True)|r| T
x:A. B(x)T